ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:ecl(ds; da), es:event_system{i:l}, i:Id.
(x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds; id-deq; x; top)))
 (e:es-E(es). (loc(e) = i)  subtype_rel(es-valtype(es; e); ma-valtype(da; es-kind(es; e))))
 (n:, e1,e2:{e:es-E(es)| loc(e) = i} . decidable((ecl-es-act(es; n; x)(e1,e2)))) 

latex

Definitions

A c B, event-info(ds;da), P  Q, x:A. B(x), ecl-trans-act(ds; da; A), ma-valtype(da; k), prop{i:l}, spreadn(a; x,y,z.t(x;y;z)), A  B, Y, t  ...$L, ge(i; j), ||as||, False, guard(T), A, P  Q, decidable(P), subtype(S; T), top, x. t(x), t  T, P  Q, x:A. B(x), if b then t else f fi , ff, tt, null(as), b, x(s), P  Q, P  Q

Lemmas

cons one one, general-append-cancellation, ecl-trans-state wf, ecl-trans-a wf, Kind-deq wf, decl-state wf, append wf, not wf, assert wf, decidable equal Kind, decidable l member, ecl-trans-ks wf, l member wf, decidable cand, last wf, last lemma, length append, length nil, length cons, non neg length, length wf1, null wf3, decidable assert, ecl-trans wf, ecl-trans-act wf, ecl-trans-property, Knd wf, fpf wf, ecl wf, event system wf, top wf, id-deq wf, fpf-cap wf, es-vartype wf, es-kind wf, ma-valtype wf, es-valtype wf, nat wf, es-loc wf, Id wf, es-E wf, event-info wf, ecl-es-act-ecl-act, es-hist wf, ecl-act wf, ecl-es-act wf, decidable functionality